1. Field
One aspect relates to methods and apparatus for use in the design and manufacture of integrated circuits, and in particular to methods and apparatus for confirming that two designs are functionally equivalent for a method of synthesis.
2. Related Art
The task of confirming that two designs are identical is one that is extremely important in all areas of hardware design. To replace an existing design in a portion of an integrated circuit with another which exhibits desirable synthesis properties, for example, first requires that a level of confidence that the two designs are functionally equivalent be attained.
When modern integrated circuit (IC) designs are produced, these usually start with a high level design specification which captures the basic functionality required but does not include the detail of implementation. High level models of this type are usually written with high level programming language to derive some proof of concept and validate the model.
Once this has been completed, the model can be reduced to register transfer level using commercially available tools. The leading producer of such tools is Synopsys. Once an RTL model has been produced, it can go through a process of optimization to determine whether portions of the design can be implemented using fewer components and areas of silicon without changing the functionality of those portions.
Two common methods used to verify whether two designs are identical are simulation of designs and formal verification, i.e., the application of formal methods to prove properties of designs. Simulation is often used for larger and more complex designs as it can effectively be employed wherever simulation of the design is possible. However, due to the ever increasing size of the input space, and the difficulty in resolving corner cases for complex designs, the confidence gained from simulation alone is becoming less and less sufficient. Formal verification, on the other hand, gives absolute confidence but is limited in applicability to small or simple designs, due to the complexity of modelling and applying formal methods.
Recently there has been growing interest in the approach of combining formal and non-formal techniques, such as simulation, as surveyed in J. Bhadra, M. S. Abadir, L.-C. Wang, S. Ray, “A Survey of Functional Verification through Hybrid Techniques”, IEEE Design & Test of Computers, March-April 2007. As demonstrated in Namrata Shekhar, Priyank Kalla, M. Brandon Meredith, and Florian Enescu “Simulation Bounds for Equivalence Verification of Polynomial Datapaths Using Finite Ring Algebra”, IEEE Transactions of Very Large Scale Integration Systems, volume 16, No. 4, April 2008. Formal properties of particular datapath designs can be used to dramatically reduce the size of the input space for such designs, allowing exhaustive simulation to be used to prove equivalence.
Commercially available tools such as Synopsys' Formality, www.synopsys.com/tools/verification/formalequivalence/pages/formality.aspx can formally prove equivalence between many designs but do not incorporate the theory of polynomial rings to simplify the verification of polynomial-like designs. Tools of this type operate at bit level to confirm functional equivalence at RTL level. However, commercially available tools are frequently unable to prove equivalence of relatively trivial designs in a reasonable time period.
Formal verification of two IC designs is a common desire in order to improve the designs of IC's and to improve the efficiency of manufacture and is realizable due to the availability of commercial products. However, the power of formal verification tools is limited, meaning that designs over a certain size or complexity cannot be successfully verified against one another.